/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;

import java.util.List;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorSyntax;
import edu.mit.csail.sdg.alloy4.ErrorType;
import edu.ut.ece382c.valloy.parser.Decl;

/**
 * Mutable; represents a predicate or function.
 *
 * <p> <b>Invariant:</b>  the list of parameters do not contain duplicates
 * <p> <b>Invariant:</b>  none of the parameter declaration contains a predicate/function call
 * <p> <b>Invariant:</b>  the return type declaration does not contain a predicate/function call
 */

public final class Func extends Node {

    /** The location in the original file where this predicate/function is declared; never null. */
    public final Pos pos;

    /** If nonnull, then this predicate/function is private (and this.isPrivate is the location of the "private" keyword) */
    public final Pos isPrivate;

    /** If nonnull, then this predicate/function is virtual (and this.isVirtual is the location of the "virtual" keyword) */
    public final Pos isVirtual;
    
    /** The label of this predicate/function; it does not need to be unique. */
    public final String label;

    /** True if this is a predicate; false if this is a function. */
    public final boolean isPred;

    /** The list of parameters; may be an empty list if this predicate/function has no parameters. */
    public final ConstList<Decl> params;

    /** The declared return type; never null. */
    public final Expr returnDecl;

    /** The predicate/function body; never null. */
    public final Expr body;
    
    /** The type of the 'this' signature reference */
    public final Expr sigRef;
    
    /** List of parameter declared types */
    public final String declTypes;
    
    /**
     * Constructs a new predicate/function.
     *
     * <p>  The first parameter's bound should be an expression with no free variables.
     * <br> The second parameter's bound should be an expression with no free variables, except possibly the first parameter.
     * <br> The third parameter's bound should be an expression with no free variables, except possibly the first two parameters.
     * <br> etc.
     * <br> The return declaration should have no free variables, except possibly the list of input parameters.
     *
     * @param pos - the original position in the file
     * @param label - the label for this predicate/function (does not have to be unique)
     * @param vars - the list of parameters (can be null or an empty list if this predicate/function has no parameters)
     * @param returnDecl - the return declaration (null if this is a predicate rather than a function)
     *
     * @throws ErrorType if returnType!=null and returnType cannot be unambiguously typechecked to be a set/relation
     * @throws ErrorSyntax if the list of parameters contain duplicates
     * @throws ErrorSyntax if at least one of the parameter declaration contains a predicate/function call
     * @throws ErrorSyntax if this function's return type declaration contains a predicate/function call
     */
    public Func(Pos pos, String label, Expr sigRef, List<Decl> vars, Expr returnDecl, Expr body) throws Err {
        this(pos, null, null, label, sigRef, vars, returnDecl, body);
    }

    /**
     * Constructs a new predicate/function.
     *
     * <p>  The first parameter's bound should be an expression with no free variables.
     * <br> The second parameter's bound should be an expression with no free variables, except possibly the first parameter.
     * <br> The third parameter's bound should be an expression with no free variables, except possibly the first two parameters.
     * <br> etc.
     * <br> The return declaration should have no free variables, except possibly the list of input parameters.
     *
     * @param pos - the original position in the file
     * @param isPrivate - if nonnull, then the user intended this func/pred to be "private"
     * @param label - the label for this predicate/function (does not have to be unique)
     * @param vars - the list of parameters (can be null or an empty list if this predicate/function has no parameters)
     * @param returnDecl - the return declaration (null if this is a predicate rather than a function)
     *
     * @throws ErrorType if returnType!=null and returnType cannot be unambiguously typechecked to be a set/relation
     * @throws ErrorSyntax if the list of parameters contain duplicates
     * @throws ErrorSyntax if at least one of the parameter declaration contains a predicate/function call
     * @throws ErrorSyntax if this function's return type declaration contains a predicate/function call
     */
    public Func(Pos pos, Pos isPrivate, Pos isVirtual, String label, Expr sigRef, List<Decl> vars, Expr returnDecl, Expr body) throws Err {
        if (pos==null) pos=Pos.UNKNOWN;
        this.pos=pos;
        this.isPrivate=isPrivate;
        this.isVirtual=isVirtual;
        this.label=(label==null ? "" : label);
        this.isPred=(returnDecl==null);
        this.returnDecl = returnDecl;
        this.params = ConstList.make(vars);
        this.body = body;
        this.sigRef = sigRef;
        
        //
        // Create a string that lists the function argument types.
        //
        String decl_string = new String();
        for(Decl d: vars) {
        	for (int i = 0; i < d.names.size(); ++i) {
        		if (decl_string.length() != 0) decl_string += ',';
        		decl_string += d.expr.toString();
        	}
        }
        
        this.declTypes = decl_string;
    }
    
    
    /** Returns a human-readable description for this predicate/function */
    @Override public final String toString()
    { 
    	StringBuilder out = new StringBuilder(); 
    	   	
    	if (isPrivate != null)
    		out.append("private ");
    	
       	if (isVirtual != null)
    		out.append("virtual ");
       	
    	if (isPred)
    		out.append("pred ");
    	else
    		out.append("fun ");
  
    	if (sigRef != null) {	
   			out.append(sigRef.toString()).append(".");
    	}
    	
		out.append(label).append(" ");
    	
    	if (params != null && params.size() != 0)
    	{	
    		String paramlist = "";
    		for(Decl d: params) {    			
    			if (paramlist.length() != 0) 
    				paramlist += ", ";
    			paramlist += d.toString();
    		}
    		
    		out.append("[" + paramlist+ "]");
    	}
    	
    	if (returnDecl != null && !isPred)
    		out.append(": " + returnDecl.toString());
    	
    	out.append(" {");
    	if (body != null) {
    		out.append('\n');
    		body.toString(out,2, true);
    		out.append('\n');
    	}
    	out.append('}');

    	return out.toString(); 
    }
    
    /** {@inheritDoc} */
    @Override public final Pos pos() { return pos; }

    /** {@inheritDoc} */
    @Override public final Pos span() { return pos; }
}
